$\forall$$T$:Type, $R$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$). \\[0ex]EquivRel($T$;$x$,$y$.$R$($x$,$y$)) $\Rightarrow$ \{$\forall$$a$, ${\it a'}$, $b$, ${\it b'}$:$T$. $R$($a$,$b$) $\Rightarrow$ $R$(${\it a'}$,${\it b'}$) $\Rightarrow$ ($R$($a$,${\it a'}$) $\Leftarrow\!\Rightarrow$ $R$($b$,${\it b'}$))\}